the_w:World, l:IdLnk, t, t':.
match(l;t;t')

||snds(l;t)||||rcvs(l;t')|| & ||rcvs(l;t')||<||snds(l;t)||+||onlnk(l;m(source(l);t))|| 

latex

Definitions	p  q, ij, snds(l;t), Action(i), destination(l), rcvs(l;t), i<j, Prop, b, P  Q, P  Q, AB, P & Q, P  Q, Msg(M), S  T, Id, Msg, mlnk(m), w.M, t  T, ||as||, onlnk(l;mss), m(i;t), source(l), x:A. B(x), , IdLnk, World, match(l;t;t')
Lemmas	world wf, IdLnk wf, nat wf, mlnk wf, lsrc wf, Id wf, w-onlnk wf, w-Msg wf, length wf1, w-M wf, Msg wf, w-m wf, le wf, assert wf, lt int wf, w-rcvs wf, ldst wf, w-action wf, w-snds wf, le int wf, band wf, assert of lt int, assert of le int, and functionality wrt iff, assert of band, iff transitivity, iff functionality wrt iff